<html>
<head><meta charset="utf-8"><title>polonius proptests · t-compiler/wg-nll · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/index.html">t-compiler/wg-nll</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html">polonius proptests</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="154093530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154093530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154093530">(Dec 31 2018 at 17:11)</a>:</h4>
<blockquote>
<p>(that is, the piece of code to generate a random set of valid facts seemed not immediately obvious but maybe it's not that hard)</p>
</blockquote>
<p>I've found that this is, hands-down, the hardest part of property-based testing.</p>
<p>That being said, we programmers implicitly do this kind of thinking all the time but don't explicitly encode it.</p>



<a name="154093656"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154093656" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154093656">(Dec 31 2018 at 17:14)</a>:</h4>
<p>"Oh, the first argument has to be less than the second argument"</p>



<a name="154093728"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154093728" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154093728">(Dec 31 2018 at 17:16)</a>:</h4>
<p>The other thing that I've found super useful is to use these types of tests to exercise variants of algorithms: "for every input, the SIMD-accelerated code must have the same results as the naive code"</p>
<p>This might be highly useful in this case as you could write "stupidly obvious" code that isn't as efficient as the <span class="emoji emoji-1f438" title="frog">:frog:</span> but it's easy to verify it's correct.</p>



<a name="154093845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154093845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154093845">(Dec 31 2018 at 17:19)</a>:</h4>
<p>are we talking about property based testing in general or the proptest crate specifically?</p>



<a name="154094013"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154094013" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154094013">(Dec 31 2018 at 17:23)</a>:</h4>
<p>PBT usually runs along the lines of 1) roundtrip (encode . decode = id, decode . encode = id), 2) test against known to be correct algorithm, 3) running a verification algorithm on a decision algorithm, e.g. <code>is_sorted</code> on the result of <code>sort</code> + then also checking that its a permutation</p>



<a name="154095279"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095279" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095279">(Dec 31 2018 at 18:00)</a>:</h4>
<p>some of my favorite PBT strategies are from <a href="https://fsharpforfunandprofit.com/pbt/" target="_blank" title="https://fsharpforfunandprofit.com/pbt/">https://fsharpforfunandprofit.com/pbt/</a></p>



<a name="154095533"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095533" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095533">(Dec 31 2018 at 18:08)</a>:</h4>
<p>funny :P; ooh! diagrams are a nice strategy -- the aspiring category theorist in me likes this</p>



<a name="154095537"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095537" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095537">(Dec 31 2018 at 18:09)</a>:</h4>
<p>the inputs seem a bit tough indeed to generate here, esp some of rustc’s liveness (if we need those facts) but some relations are easier than others; the test text parser already shows some of these validity rules / fact generation —definitely interesting</p>



<a name="154095541"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095541" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095541">(Dec 31 2018 at 18:09)</a>:</h4>
<p><span class="user-mention" data-user-id="116113">@lqd</span>  yeah graphs are usually hard to generate I find</p>



<a name="154095550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095550">(Dec 31 2018 at 18:10)</a>:</h4>
<p><span class="user-mention" data-user-id="116113">@lqd</span> have you tried the proptest crate?</p>



<a name="154095597"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095597" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095597">(Dec 31 2018 at 18:10)</a>:</h4>
<p>(even reusing rustc might have been an option :)</p>



<a name="154095598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095598">(Dec 31 2018 at 18:10)</a>:</h4>
<p>I'm biased (since I wrote some of that code...) but it's pretty ergonomic to use</p>



<a name="154095609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095609">(Dec 31 2018 at 18:11)</a>:</h4>
<p>only quickcheck myself but I think niko has added some tests using it to datafrog</p>



<a name="154095618"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095618" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095618">(Dec 31 2018 at 18:11)</a>:</h4>
<p>/me looks</p>



<a name="154095709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095709">(Dec 31 2018 at 18:13)</a>:</h4>
<p>cool</p>



<a name="154095772"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095772" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095772">(Dec 31 2018 at 18:14)</a>:</h4>
<p><span class="user-mention" data-user-id="116113">@lqd</span>  we're working on a book + shipping <code>#[derive(Arbitrary)]</code> which should remove some of the boilerplate</p>



<a name="154095777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095777">(Dec 31 2018 at 18:14)</a>:</h4>
<p>nice!</p>



<a name="154095802"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095802" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095802">(Dec 31 2018 at 18:15)</a>:</h4>
<p>I hope we’ll use it more then :)</p>



<a name="154095805"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095805" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095805">(Dec 31 2018 at 18:15)</a>:</h4>
<p>:P</p>



<a name="154095866"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095866" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095866">(Dec 31 2018 at 18:17)</a>:</h4>
<p><span class="user-mention" data-user-id="116113">@lqd</span> it would be nice to get CoArbitrary to work as well to proptest some HoFs and such; I spoke to Koen about it a while back but it was sorta tricky to implement without GADTs so I put it on hold</p>



<a name="154095939"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154095939" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154095939">(Dec 31 2018 at 18:18)</a>:</h4>
<p>:)</p>



<a name="154099778"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154099778" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154099778">(Dec 31 2018 at 20:09)</a>:</h4>
<p>I still love the post about using QuickCheck to test an entire C application</p>



<a name="154099785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154099785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154099785">(Dec 31 2018 at 20:09)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span> is that John's article?</p>



<a name="154099868"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154099868" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154099868">(Dec 31 2018 at 20:11)</a>:</h4>
<p><a href="https://pdfs.semanticscholar.org/76c7/ddcaadee1fc0b475df59c08bf0700313586d.pdf" target="_blank" title="https://pdfs.semanticscholar.org/76c7/ddcaadee1fc0b475df59c08bf0700313586d.pdf">https://pdfs.semanticscholar.org/76c7/ddcaadee1fc0b475df59c08bf0700313586d.pdf</a> ? Seems likely</p>



<a name="154099941"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154099941" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154099941">(Dec 31 2018 at 20:13)</a>:</h4>
<p>Ah; nice one -- I really like this paper: <a href="https://dl.acm.org/citation.cfm?id=2364516" target="_blank" title="https://dl.acm.org/citation.cfm?id=2364516">https://dl.acm.org/citation.cfm?id=2364516</a></p>



<a name="154100668"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154100668" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154100668">(Dec 31 2018 at 20:32)</a>:</h4>
<p>That link doesn't provide a way to read the article without paying, is that correct?</p>



<a name="154100682"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154100682" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154100682">(Dec 31 2018 at 20:33)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span>  yeah sadly; here's a talk Koen held about it: <a href="https://www.youtube.com/watch?v=CH8UQJiv9Q4" target="_blank" title="https://www.youtube.com/watch?v=CH8UQJiv9Q4">https://www.youtube.com/watch?v=CH8UQJiv9Q4</a></p>
<div class="youtube-video message_inline_image"><a data-id="CH8UQJiv9Q4" href="https://www.youtube.com/watch?v=CH8UQJiv9Q4" target="_blank" title="https://www.youtube.com/watch?v=CH8UQJiv9Q4"><img src="https://i.ytimg.com/vi/CH8UQJiv9Q4/default.jpg"></a></div>



<a name="154100692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154100692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154100692">(Dec 31 2018 at 20:33)</a>:</h4>
<p>implemented here: <a href="http://hackage.haskell.org/package/QuickCheck-2.12.6.1/docs/Test-QuickCheck-Function.html" target="_blank" title="http://hackage.haskell.org/package/QuickCheck-2.12.6.1/docs/Test-QuickCheck-Function.html">http://hackage.haskell.org/package/QuickCheck-2.12.6.1/docs/Test-QuickCheck-Function.html</a></p>



<a name="154100876"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154100876" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154100876">(Dec 31 2018 at 20:38)</a>:</h4>
<p><span class="user-mention" data-user-id="116155">@Jake Goulding</span>  Fortunately I found it in my stash :P  <a href="/user_uploads/4715/ecH2ys-MIMPJ3oTnE3vSesjS/p73-claessen.pdf" target="_blank" title="p73-claessen.pdf">p73-claessen.pdf</a></p>



<a name="154103794"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122657-t-compiler/wg-nll/topic/polonius%20proptests/near/154103794" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122657-t-compiler/wg-nll/topic/polonius.20proptests.html#154103794">(Dec 31 2018 at 22:09)</a>:</h4>
<p>cough sci-hub cough</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>